COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	airpor[w83,jmc]		Axioms for the airport problem
C00009 ENDMK
C⊗;
airpor[w83,jmc]		Axioms for the airport problem

These axioms are an updated version of the airport axioms given in
"Programs with Common Sense" and are meant to be read in conjunction
with that paper.  They use the situtation calculus of "Some Philosophical
Problems from the Standpoint of Artificial Intelligence", so maybe you'd
better recall that paper also.

1. want(at(I,airport),s0)

Here we have already reified  at(I,airport)  so it can be something
we want.

2. holds(at(I,desk),s0)

This takes the form it does in consequence of the previous decision
to reify  at(I,airport).  Otherwise it might be  at(I,airport,s0).

3. att(desk,home).

We could use  holds(at(desk,home),s0)  but then we would
need frame axioms to ensure that the desk remained at home when we
walked to the car.  We'll need frame axioms anyway to keep the
car at home.

4. holds(at(car,home),s0)

5. att(home,county)

6. att(airport,county)

7. walkable(home)

8. drivable(county)

We might write
9*. ∀x y z s.holds(at(I,x),s) ∧ holds(at(x,z),s) ∧ holds(at(y,z),s) ∧ walkable(z)
	⊃ holds(at(I,y),result(walk-to(y),s)).

This first attempt at giving the effect of walking isn't good enough
for two reasons.  We are using the linguists' convention of putting *
next to sentences that aren't quite right.
First, we have  att(desk,home)  rather than the
holds(at(desk,home),s), but this is easily fixed by writing

10. ∀x y.att(x,y) ⊃ ∀s.holds(at(x,y),s)

We could write ≡ instead of ⊃, but let's be conservative, and hold off
making this relation an equivalence.  We don't need it now, and we should
refrain until we have an example in which it is used.
Anther alternative is to write  (holds(at(x,z),s) ∨ att(x,z)) as the premiss
of 9*.  I like 10 better, and I think we'll often want relations like 10
relating situation-dependent and situation independent versions of relations.

The other problem with 9* is the famous frame problem.  We'll need to
show that in the situation  result(walk-to(car),s0), the car is still at
home.  This is the famous frame problem.  My current panacea for fram
problems is circumscription, which I'll come to later, so I'll modify
9* sufficiently to give the right answer in this case, and you can
criticize its ad hoc character, i.e. its unsuitableness for inclusion
in a general purpose database of common sense facts.

We therefore have

9. ∀x y z s.holds(at(I,x),s) ∧ holds(at(x,z),s) ∧ holds(at(y,z),s) ∧ walkable(z)
	⊃ [λs'.holds(at(I,y),s') 
		∧ ∀o p.o ≠ x ⊃ holds(at(o,p),s') ≡ holds(at(o,p),s)]
			(result(go-to(y),s)).

Here the λ-expression is used just to save writing  result(go-to(y),s)
twice.  This axiom is incompatible with the transitivity of  at; why?

11. ∀w x y z s.is-car(w) ∧ holds(at(I,w),s) ∧ holds(at(w,x),s) ∧
		holds(at(x,z),s) ∧ holds(at(y,z),s) ∧ drivable(z)
		⊃ [λs'.holds(at(I,w),s') ∧ holds(at(w,y),s')
			∧ ∀o p.o ≠ I ⊃ holds(at(o,p),s') ≡ holds(at(o,p),s)]
			(result(drive-to(y),s)).

12. is-car(car).
We could have replaced the first two conjuncts of 11 by holds(at(I,car),s),
but then our axiom about the effect of driving would apply to the
particular car named "car", and this would be ad hoc beyond even the
relaxed standards of this treatment.

The above axioms are sufficient to show that

[λs''.holds(at(I,car),s'') ∧ holds(at(car,airport),s'')]
		(result(drive(airport),result(walk(car),s0))).

Of course, our first order proof-checker had better allow first order
lambdas.

All this has not used  want(at(I,airport),s0),  and we need additional
axioms to show  should(go(car),s0).

Which of the following axioms is redundant?

13. ∀p a s.want(p,s) ∧ holds(p,result(a,s)) ⊃ should(a,s)

14. ∀p s.holds(p,s) ⊃ can(p,s)

15. ∀p a s.can(p,result(a,s)) ⊃ can(p,s)

16. ∀p a s.wants(p,s) ∧ can(p,result(a,s)) ⊃ should(a,s)

Naturally, the above axioms have the objection that any action that
will achieve the goal should be done.